第4章 構造化プログラミング
制限のない制御の移行(goto文)をなくした
ダイクストラ(Dijkstra)
goto文を使うことによって、モジュールを再帰的に小さな単位に分割できなくなること、それにより合理的な証明に欠かせない「分割統治」が使えなくなることを発見した。(Kindle の位置No.660-662)
goto文を選択と反復に限る
構造化プログラミングを誕生させた
その2年前にBöhmとJacopiniが、あらゆるプログラムは「順次」「選択」「反復」の3つの構造で構築できることを特定していた (Kindle の位置No.667-669)
モジュールを証明可能にする制御構造は、あらゆるプログラムを構築できる制御構造の最小セットと同じ (Kindle の位置No.669-670)
(構造化定理の順次・選択・反復であればモジュールは証明可能となる)
ダイクストラは数学として証明しようとしたが、実際は科学における証明となった
テストによる反証可能性
プログラムが正しくないことは証明できる
プログラムが正しいことは証明できない
どれだけ最善を尽くしても正しくないことを証明できないことによって、その正しさを明らかにしているのである。(Kindle の位置No.733-734)
テストが正しくないことを証明できない(テストがパスする)
その場合、その機能は正しいとみなせる